// Generated from mccproperty.g by ANTLR 4.0
package parser;

import java.util.ArrayList;
import java.util.Hashtable;
import java.util.Iterator;
import java.util.List;
import org.antlr.v4.runtime.ParserRuleContext;
import org.antlr.v4.runtime.TokenStream;
import parser.mccpropertyParser.PropertyContext;
import properties.Property;

//TODO Gestire W
class Translator extends mccpropertyBaseListener {

    private mccpropertyParser parser;
    private boolean comparerSub;
    private List<Property> properties;
    private TokenStream tokens;
    private StringBuilder currentProperty;
    private Property current;
    private int braceLiveCounter;
    private Hashtable<ParserRuleContext, String> printOnExit;
    private Hashtable<ParserRuleContext, String> actuallyPrinted;//QUESTA DEVE ESSERE DI STRINGBUILDER
    private Hashtable<ParserRuleContext, String> replace;

    public Translator(mccpropertyParser parser, boolean comparerSub) {
        this.parser = parser;
        tokens = parser.getTokenStream();
        properties = new ArrayList<>();//Java7
        currentProperty = new StringBuilder();
        this.comparerSub = comparerSub;
        printOnExit = new Hashtable<>(1000000);
        replace = new Hashtable<>();
        actuallyPrinted = new Hashtable<>(1000000);

        braceLiveCounter = 0;
    }

    public List<Property> getProperties() {
        return properties;
    }

    @Override
    public void enterComparer(mccpropertyParser.ComparerContext ctx) {
        if (replace.containsKey(ctx)) {
            currentProperty.append(replace.get(ctx)+" ");
            replace.remove(ctx);
        } else {
            currentProperty.append(tokens.getText(ctx)+" ");
        }
    }

    @Override
    public void enterInteger(mccpropertyParser.IntegerContext ctx) {
        currentProperty.append(tokens.getText(ctx)+" ");
    }

    @Override
    public void enterProperty_set(mccpropertyParser.Property_setContext ctx) {
        Iterator i = ctx.children.iterator();
        while (i.hasNext()) {
            mccpropertyParser.PropertyContext property = (mccpropertyParser.PropertyContext) i.next();
            String startsWith = property.getChild(0).getText();
            String formula = tokens.getText(property.complex_formula());
            if (formula.contains("bound")
                    || "ltl".equals(startsWith)
                    || formula.contains("~")
                    || formula.contains("l2")
                    || formula.contains(",")) {
                i.remove();
            }

        }
    }

    @Override
    public void enterProperty(mccpropertyParser.PropertyContext ctx) {
        current = new Property();
        properties.add(current);
        current.setName(tokens.getText(ctx.identifier()));
        currentProperty = new StringBuilder();
    }

    @Override
    public void exitProperty(mccpropertyParser.PropertyContext ctx) {
        current.setProperty(tokens.getText(ctx.complex_formula()));
        current.setTranslation(currentProperty.toString().replaceAll("  ", " "));
    }

    @Override
    public void enterMop(mccpropertyParser.MopContext ctx) {
        String mop = tokens.getText(ctx);
        switch (mop) {//Java7
            case "&":
                currentProperty.append(" and ");
                return;
            case "|":
                currentProperty.append(" or ");
                return;
            default:
                throw new RuntimeException("Token non riconosciuto: " + mop);
        }
    }

    @Override
    public void enterIfs(mccpropertyParser.IfsContext ctx) {
        //Questa divisione degli if è poco funzionale.
        String ifs = tokens.getText(ctx);
        if ("=>".equals(ifs)) {
            currentProperty.append(" -> ");
        }
    }

    @Override
    public void enterOperator(mccpropertyParser.OperatorContext ctx) {
        String operator = tokens.getText(ctx);
        switch (operator) {//Java7
            case "I":
                currentProperty.append(" A G ");
                return;
            case "N":
                currentProperty.append(" not E F ");
                return;
            default:
                currentProperty.append(" "+operator+" ");
        }
    }

    @Override
    public void enterNot(mccpropertyParser.NotContext ctx) {
        currentProperty.append(" not ");
    }

    @Override
    public void enterIdentifier(mccpropertyParser.IdentifierContext ctx) {
        if (!(ctx.getParent() instanceof mccpropertyParser.PropertyContext)) {//per evitare il nome della formula
            currentProperty.append(tokens.getText(ctx)+" ");
        }

    }

    @Override
    public void enterSimple_formula_next(mccpropertyParser.Simple_formula_nextContext ctx) {
        //Se contiene ~ non può essere tradotta
        int xs = 1;
        if (ctx.integer() != null) {
            xs = Integer.parseInt(tokens.getText(ctx.integer()));
        }
        for (int i = 0; i < xs; i++) {
            currentProperty.append(" X ");
        }
    }

    @Override
    public void enterSimple_formula_liveness(mccpropertyParser.Simple_formula_livenessContext ctx) {
        braceLiveCounter = 1;//Nota: non ne ci sono anndiate
        if (ctx.children.size() == 3) {
            switch (ctx.getChild(2).getText()) {//Java7
                case "l0":
                    currentProperty.append(" not E F (");
                    braceLiveCounter++;
                    break;
                case "l1":
                    currentProperty.append(" E F (");
                    braceLiveCounter++;
                    break;
                case "l2":
                    throw new RuntimeException("l2 found");
                case "l3":
                    currentProperty.append(" E F A G E F (");
                    braceLiveCounter++;
                    break;
                case "l4":
                    currentProperty.append(" A G E F (");
                    braceLiveCounter++;
                    break;
            }
        }
        currentProperty.append(" en(");

    }

    @Override
    public void exitSimple_formula_liveness(mccpropertyParser.Simple_formula_livenessContext ctx) {
        for (int i = 0; i < braceLiveCounter; i++) {
            currentProperty.append(")");
        }
    }

    @Override
    public void enterSimple_formula_comparer(mccpropertyParser.Simple_formula_comparerContext ctx) {
        /*
         * Qui bisogna, nel caso comparerSub, far diventare P C P in P - P C 0
         * Si potrebbe fare in diversi modi, l'unico in cui sono riuscito è:
         * Trasformo P C P in P P Alla exit del primo P stampo il -, che mi
         * salvo su una hashtable (il - è legato all'oggetto contesto)
         * all'uscita di questo nodo padre stamp il C 0 che è salvato anch'esso
         * sull'hashtable.
         *
         */
        String comparer = tokens.getText(ctx.comparer());
        mccpropertyParser.Complex_expressionContext arg1 = ctx.complex_expression(0);
        mccpropertyParser.Complex_expressionContext arg2 = ctx.complex_expression(1);
        if (comparerSub || !("=".equals(comparer) || "!=".equals(comparer))) {
            while (ctx.getChildCount() > 0) {
                ctx.removeLastChild();
            }
            ctx.addChild(arg1);
            printOnExit.put(arg1, " - ");
            ctx.addChild(arg2);
            printOnExit.put(ctx, comparer + " 0 ");

        } else {
            if (!isInt(arg1.getText()) && !isInt(arg2.getText())) {
                String newComparer;
                switch (comparer) {//Java7
                    case "=":
                        newComparer = "==";
                        break;
                    case "!=":
                        newComparer = "<>";
                        break;
                    default:
                        newComparer = comparer;//TODO
                }
                replace.put(ctx.comparer(), newComparer);
            }
        }

    }

    @Override
    public void enterSimple_formula_const(mccpropertyParser.Simple_formula_constContext ctx) {
        currentProperty.append(" ").append(ctx.getChild(0)+" ");
    }

    @Override
    public void enterSimple_formula(mccpropertyParser.Simple_formulaContext ctx) {
        if (ctx.complex_formula() != null && ctx.complex_formula().untils()==null) {
            currentProperty.append("(");

        }

    }

    @Override
    public void exitSimple_formula(mccpropertyParser.Simple_formulaContext ctx) {
        if (ctx.complex_formula() != null && ctx.complex_formula().untils()==null) {
            currentProperty.append(")");
        }
    }

    @Override
    public void enterComplex_formula(mccpropertyParser.Complex_formulaContext ctx) {
        if (ctx.xor() != null) {
            /*
             * A xor B = A or B and not (A and B) oppure A xor B = A and not B
             * or not A and B
             *
             * Qual è meglio?
             *
             *
             * AB -> (A [and not] B[) or (not ]A [and ] B[)]
             *
             */
            mccpropertyParser.Simple_formulaContext arg1 = ctx.simple_formula(0);
            mccpropertyParser.Simple_formulaContext arg2 = ctx.simple_formula(1);
            currentProperty.append("(");

            /*
             * Atenzione a non sovrascrivere!
             */
            printOnExit.put(arg1, " and not ");//valgono solo per i primi
            printOnExit.put(arg2, ") or (not ");
            //gli altri due li aggiungo all'exit
        } else if (ctx.ifs() != null && tokens.getText(ctx.ifs()).equals("<=>")) {
            /*
             * AB -> (A -> B) and (B -> A)
             *
             */
            mccpropertyParser.Simple_formulaContext arg1 = ctx.simple_formula(0);
            mccpropertyParser.Simple_formulaContext arg2 = ctx.simple_formula(1);
            currentProperty.append("(");
            printOnExit.put(arg1, "->");
            printOnExit.put(arg2, ") and (");
        }
        if(ctx.untils()!=null){
            mccpropertyParser.Simple_formulaContext arg1 = ctx.simple_formula(0);
            mccpropertyParser.Simple_formulaContext arg2 = ctx.simple_formula(1);
            printOnExit.put(arg1," U ");
            printOnExit.put(arg2,"] ");
            currentProperty.append(" [");
        }
        //TODO W
    }

    @Override
    public void exitComplex_formula(mccpropertyParser.Complex_formulaContext ctx) {
        if (ctx.xor() != null) {
            currentProperty.append(actuallyPrinted.get(ctx.simple_formula(0))+" ");
            currentProperty.append(" and ");
            currentProperty.append(actuallyPrinted.get(ctx.simple_formula(1))+" ");
            currentProperty.append(")");
        } else if (ctx.ifs() != null && tokens.getText(ctx.ifs()).equals("<=>")) {
            currentProperty.append(actuallyPrinted.get(ctx.simple_formula(1))+" ");
            currentProperty.append(" -> ");
            currentProperty.append(actuallyPrinted.get(ctx.simple_formula(0))+" ");
            currentProperty.append(")");
        }
    }

    @Override
    public void enterAlgebra_operatorm(mccpropertyParser.Algebra_operatormContext ctx) {
        currentProperty.append(tokens.getText(ctx)+" ");
    }

    @Override
    public void enterAlgebra_operator(mccpropertyParser.Algebra_operatorContext ctx) {
        currentProperty.append(tokens.getText(ctx)+" ");
    }

    @Override
    public void enterSimple_expression(mccpropertyParser.Simple_expressionContext ctx) {
        if (ctx.complex_expression() != null) {
            currentProperty.append("(");

        }
    }

    @Override
    public void exitSimple_expression(mccpropertyParser.Simple_expressionContext ctx) {
        if (ctx.complex_expression() != null) {
            currentProperty.append(")");
        }
        
    }



    @Override
    public void enterEveryRule(ParserRuleContext ctx) {
        actuallyPrinted.put(ctx, currentProperty.toString());
    }

    @Override
    public void exitEveryRule(ParserRuleContext ctx) {

        //Un po' bruttino, nè?
        if (!(ctx instanceof PropertyContext)) {
            String was = actuallyPrinted.remove(ctx);
            if (!currentProperty.toString().equals(was)) {
                actuallyPrinted.put(ctx, currentProperty.toString().substring(was.length()));
            }
        }
        String poe = printOnExit.remove(ctx);
        if (poe != null) {
            currentProperty.append(poe+" ");
        }


    }

    private boolean isInt(String s) {
        try {
            Integer.parseInt(s);
            return true;
        } catch (Exception e) {

            return false;
        }
    }
}